Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(app(compose,f),g),x)  → app(g,app(f,x))
2:    app(reverse,l)  → app(app(reverse2,l),nil)
3:    app(app(reverse2,nil),l)  → l
4:    app(app(reverse2,app(app(cons,x),xs)),l)  → app(app(reverse2,xs),app(app(cons,x),l))
5:    app(hd,app(app(cons,x),xs))  → x
6:    app(tl,app(app(cons,x),xs))  → xs
7:    last  → app(app(compose,hd),reverse)
8:    init  → app(app(compose,reverse),app(app(compose,tl),reverse))
There are 13 dependency pairs:
9:    APP(app(app(compose,f),g),x)  → APP(g,app(f,x))
10:    APP(app(app(compose,f),g),x)  → APP(f,x)
11:    APP(reverse,l)  → APP(app(reverse2,l),nil)
12:    APP(reverse,l)  → APP(reverse2,l)
13:    APP(app(reverse2,app(app(cons,x),xs)),l)  → APP(app(reverse2,xs),app(app(cons,x),l))
14:    APP(app(reverse2,app(app(cons,x),xs)),l)  → APP(reverse2,xs)
15:    APP(app(reverse2,app(app(cons,x),xs)),l)  → APP(app(cons,x),l)
16:    LAST  → APP(app(compose,hd),reverse)
17:    LAST  → APP(compose,hd)
18:    INIT  → APP(app(compose,reverse),app(app(compose,tl),reverse))
19:    INIT  → APP(compose,reverse)
20:    INIT  → APP(app(compose,tl),reverse)
21:    INIT  → APP(compose,tl)
The approximated dependency graph contains one SCC: {9-11,13}.
Tyrolean Termination Tool  (0.07 seconds)   ---  May 3, 2006